T:Type, l:(T List), i:{0..||l||}, j:{0..i}. last(l_interval(l;j;i)) = l[(i - 1)]  T 

latex

Definitions	x:A. B(x), {i..j}, last(L), P  Q, P  Q, t  T, i  j < k, P & Q, P  Q, , SQType(T), {T}, T, A  B, True, A, False
Lemmas	select l interval, le wf, length l interval, select wf, int seg wf, length wf1, squash wf